\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Config}$:AbsInterface(chain\_config()), ${\it Cmd}$:Type, ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)),\+
\\[0ex]$e$:E.
\-\\[0ex]cmd{-}history($e$) $\in$ (${\it Cmd}$ List)
\end{tabbing}